// Przykładowe drzewo przeszukiwania w składni racklogowej
// autor: Tomasz Drab (tdr@cs.uni.wroc.pl)
// autor oryginału: Tomasz Wierzbicki
// data: 19 lutego 2020 r.
// licencja: CC-BY

digraph "drzewo przeszukiwania" {
  graph [fontname = "sans"]
  node [fontname = "sans" shape = "none"]
  edge [fontname = "sans"]

  labelloc=t
  labeljust=l
  label = "        (define %append\l           (%rel (x h t s)\l (1)        [('() x x)]\l (2)        [((cons h t) x (cons h s))\l                 (%append t x s)]))\l\l(%which (x y) (%append x y '(a b)))\l\l"

  //Poniższa kolejność definicji odpowiada kolejności rysowania drzewa.

  //Początkowy węzeł na liście celów ma tylko jeden cel pochodzący z %which.
  2 [label = "(%append x y '(a b))"]

  //Zmiennym pochodzącym z definicji relacji, w celu uniknięcia konfliktu nazw,
  //dodajemy aktualny poziom drzewa za indeks dolny.
  2 -> 1 [label = "(1)\nx := '()\lx₁ := '(a b)\ly := '(a b)\l"]

  //Lista celów jest pusta — sukces.
  1 [label = "☺\nx = '()\ly = '(a b)"]

  //Lepiej oryginalne zmienne podstawiać pod nowe zmienne,
  //żeby łatwiej było odczytać wynik.
  2 -> 4 [label = "(2)\nx := (cons 'a t₁)\lh₁ := 'a\ls₁ := '(b)\lx₁ := y\l"]

  //Do listy celów dodawane są wszystkie warunki rozważanej reguły.
  //W tym przypadku jeden warunek.
  4 [label = "(%append t₁ y '(b))"]

  4 -> 3 [label = "(1)\nt₁ := '()\lx₂ := '(b)\ly := '(b)\l"]
  3 [label = "☺\nx = '(a)\ly = '(b)\l"]
  4 -> 6 [label = "(2)\nt₁ := (cons 'b t₂)\lh₂ := 'b\ls₂ := '()\lx₂ := y\l"]
  6 [label = "(%append t₂ y '())"]
  6 -> 5 [label = "(1)\nt₂ := '()\lx₃ := '()\ly := '()\l"]
  5 [label = "☺\nx = '(a b)\ly = '()\l"]
  6 -> 7 [label = "(2)\n(cons h₃ s₃)\lnie unifikuje się z\l'()\l"]
  7 [label = "☹\n\n\n"]
}